$\forall$$T$:Type, $t$:$T$, $l$:IdLnk, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $f$:(State(${\it ds}$)$\rightarrow$($T$ + Top)).
\\[0ex]Normal(${\it ds}$) $\Rightarrow$ $\vdash$${\it es}$.weak{-}send{-}do{-}apply(${\it es}$;$T$;$l$;"tg";"a";${\it ds}$;$f$)